<?php

/**
 * Configuration settings, for everything we don't want to store in the
 * config file - ie, hopefully, everything but the database settings.
 */
class config extends thingy {
}

?>
